H-Termination proof of /home/matraf/haskell/eval_FullyBlown

YES 1.707 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:

↳ HASKELL

  ↳ BR

mainModule List

((nub :: [Ordering] -> [Ordering]) :: [Ordering] -> [Ordering])

module List where

import qualified Maybe
import qualified Prelude

nub :: Eq a => [a] -> [a]

nub

nub' l []

where

nub'

[] _

[]

nub'

(x : xs) ls

x `elem` ls

nub' xs ls

otherwise

x : nub' xs (x : ls)

module Maybe where

import qualified List
import qualified Prelude

Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

mainModule List

((nub :: [Ordering] -> [Ordering]) :: [Ordering] -> [Ordering])

module List where

import qualified Maybe
import qualified Prelude

nub :: Eq a => [a] -> [a]

nub

nub' l []

where

nub'

[] vw

[]

nub'

(x : xs) ls

x `elem` ls

nub' xs ls

otherwise

x : nub' xs (x : ls)

module Maybe where

import qualified List
import qualified Prelude

Cond Reductions:
The following Function with conditions

nub' [] vw = []

nub' (x : xs) ls

| x `elem` ls

= nub' xs ls

| otherwise

= x : nub' xs (x : ls)

is transformed to

nub' [] vw = nub'3 [] vw

nub' (x : xs) ls = nub'2 (x : xs) ls

nub'0 x xs ls True = x : nub' xs (x : ls)

nub'1 x xs ls True = nub' xs ls

nub'1 x xs ls False = nub'0 x xs ls otherwise

nub'2 (x : xs) ls = nub'1 x xs ls (x `elem` ls)

nub'3 [] vw = []

nub'3 wv ww = nub'2 wv ww

The following Function with conditions

undefined

| False

= undefined

is transformed to

undefined = undefined1

undefined0 True = undefined

undefined1 = undefined0 False

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ LetRed

mainModule List

((nub :: [Ordering] -> [Ordering]) :: [Ordering] -> [Ordering])

module List where

import qualified Maybe
import qualified Prelude

nub :: Eq a => [a] -> [a]

nub

nub' l []

where

nub'	[] vw	=	nub'3 [] vw
nub'	(x : xs) ls	=	nub'2 (x : xs) ls

nub'0

x xs ls True

x : nub' xs (x : ls)

nub'1	x xs ls True	=	nub' xs ls
nub'1	x xs ls False	=	nub'0 x xs ls otherwise

nub'2

(x : xs) ls

nub'1 x xs ls (x `elem` ls)

nub'3	[] vw	=	[]
nub'3	wv ww	=	nub'2 wv ww

module Maybe where

import qualified List
import qualified Prelude

Let/Where Reductions:
The bindings of the following Let/Where expression

nub' l []

where

nub' [] vw = nub'3 [] vw

nub' (x : xs) ls = nub'2 (x : xs) ls

nub'0 x xs ls True = x : nub' xs (x : ls)

nub'1 x xs ls True = nub' xs ls

nub'1 x xs ls False = nub'0 x xs ls otherwise

nub'2 (x : xs) ls = nub'1 x xs ls (x `elem` ls)

nub'3 [] vw = []

nub'3 wv ww = nub'2 wv ww

are unpacked to the following functions on top level

nubNub' [] vw = nubNub'3 [] vw

nubNub' (x : xs) ls = nubNub'2 (x : xs) ls

nubNub'2 (x : xs) ls = nubNub'1 x xs ls (x `elem` ls)

nubNub'1 x xs ls True = nubNub' xs ls

nubNub'1 x xs ls False = nubNub'0 x xs ls otherwise

nubNub'3 [] vw = []

nubNub'3 wv ww = nubNub'2 wv ww

nubNub'0 x xs ls True = x : nubNub' xs (x : ls)

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ LetRed

            ↳ HASKELL

              ↳ Narrow

mainModule List

(nub :: [Ordering] -> [Ordering])

module List where

import qualified Maybe
import qualified Prelude

nub :: Eq a => [a] -> [a]

nub

nubNub' l []

nubNub'	[] vw	=	nubNub'3 [] vw
nubNub'	(x : xs) ls	=	nubNub'2 (x : xs) ls

nubNub'0

x xs ls True

x : nubNub' xs (x : ls)

nubNub'1	x xs ls True	=	nubNub' xs ls
nubNub'1	x xs ls False	=	nubNub'0 x xs ls otherwise

nubNub'2

(x : xs) ls

nubNub'1 x xs ls (x `elem` ls)

nubNub'3	[] vw	=	[]
nubNub'3	wv ww	=	nubNub'2 wv ww

module Maybe where

import qualified List
import qualified Prelude

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="nub",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="nub wx3",fontsize=16,color="black",shape="triangle"];3 -> 4[label="",style="solid", color="black", weight=3];
4[label="nubNub' wx3 []",fontsize=16,color="burlywood",shape="box"];941[label="wx3/wx30 : wx31",fontsize=10,color="white",style="solid",shape="box"];4 -> 941[label="",style="solid", color="burlywood", weight=9];
941 -> 5[label="",style="solid", color="burlywood", weight=3];
942[label="wx3/[]",fontsize=10,color="white",style="solid",shape="box"];4 -> 942[label="",style="solid", color="burlywood", weight=9];
942 -> 6[label="",style="solid", color="burlywood", weight=3];
5[label="nubNub' (wx30 : wx31) []",fontsize=16,color="black",shape="box"];5 -> 7[label="",style="solid", color="black", weight=3];
6[label="nubNub' [] []",fontsize=16,color="black",shape="box"];6 -> 8[label="",style="solid", color="black", weight=3];
7[label="nubNub'2 (wx30 : wx31) []",fontsize=16,color="black",shape="box"];7 -> 9[label="",style="solid", color="black", weight=3];
8[label="nubNub'3 [] []",fontsize=16,color="black",shape="box"];8 -> 10[label="",style="solid", color="black", weight=3];
9[label="nubNub'1 wx30 wx31 [] (wx30 `elem` [])",fontsize=16,color="black",shape="box"];9 -> 11[label="",style="solid", color="black", weight=3];
10[label="[]",fontsize=16,color="green",shape="box"];11[label="nubNub'1 wx30 wx31 [] (any . (==))",fontsize=16,color="black",shape="box"];11 -> 12[label="",style="solid", color="black", weight=3];
12[label="nubNub'1 wx30 wx31 [] (any ((==) wx30) [])",fontsize=16,color="black",shape="box"];12 -> 13[label="",style="solid", color="black", weight=3];
13 -> 404[label="",style="dashed", color="red", weight=0];
13[label="nubNub'1 wx30 wx31 [] (or . map ((==) wx30))",fontsize=16,color="magenta"];13 -> 405[label="",style="dashed", color="magenta", weight=3];
13 -> 406[label="",style="dashed", color="magenta", weight=3];
13 -> 407[label="",style="dashed", color="magenta", weight=3];
405[label="wx31",fontsize=16,color="green",shape="box"];406[label="[]",fontsize=16,color="green",shape="box"];407[label="wx30",fontsize=16,color="green",shape="box"];404[label="nubNub'1 wx5 wx6 wx7 (or . map ((==) wx5))\n  Eq a",fontsize=16,color="black",shape="triangle"];404 -> 447[label="",style="solid", color="black", weight=3];
447[label="nubNub'1 wx5 wx6 wx7 (or (map ((==) wx5) wx7))\n  Eq a",fontsize=16,color="black",shape="box"];447 -> 448[label="",style="solid", color="black", weight=3];
448[label="nubNub'1 wx5 wx6 wx7 (foldr (||) False (map ((==) wx5) wx7))\n  Eq a",fontsize=16,color="burlywood",shape="box"];944[label="wx7/wx70 : wx71",fontsize=10,color="white",style="solid",shape="box"];448 -> 944[label="",style="solid", color="burlywood", weight=9];
944 -> 449[label="",style="solid", color="burlywood", weight=3];
945[label="wx7/[]",fontsize=10,color="white",style="solid",shape="box"];448 -> 945[label="",style="solid", color="burlywood", weight=9];
945 -> 450[label="",style="solid", color="burlywood", weight=3];
449[label="nubNub'1 wx5 wx6 (wx70 : wx71) (foldr (||) False (map ((==) wx5) (wx70 : wx71)))\n  Eq a",fontsize=16,color="black",shape="box"];449 -> 451[label="",style="solid", color="black", weight=3];
450[label="nubNub'1 wx5 wx6 [] (foldr (||) False (map ((==) wx5) []))\n  Eq a",fontsize=16,color="black",shape="box"];450 -> 452[label="",style="solid", color="black", weight=3];
451 -> 822[label="",style="dashed", color="red", weight=0];
451[label="nubNub'1 wx5 wx6 (wx70 : wx71) (foldr (||) False (((==) wx5 wx70) : map ((==) wx5) wx71))\n  Eq a",fontsize=16,color="magenta"];451 -> 823[label="",style="dashed", color="magenta", weight=3];
451 -> 824[label="",style="dashed", color="magenta", weight=3];
451 -> 825[label="",style="dashed", color="magenta", weight=3];
451 -> 826[label="",style="dashed", color="magenta", weight=3];
451 -> 827[label="",style="dashed", color="magenta", weight=3];
451 -> 828[label="",style="dashed", color="magenta", weight=3];
452[label="nubNub'1 wx5 wx6 [] (foldr (||) False [])\n  Eq a",fontsize=16,color="black",shape="box"];452 -> 454[label="",style="solid", color="black", weight=3];
823[label="wx71\n  Eq a",fontsize=16,color="green",shape="box"];824[label="wx6\n  Eq a",fontsize=16,color="green",shape="box"];825[label="wx70\n  Eq a",fontsize=16,color="green",shape="box"];826[label="wx71\n  Eq a",fontsize=16,color="green",shape="box"];827[label="wx70\n  Eq a",fontsize=16,color="green",shape="box"];828[label="wx5\n  Eq a",fontsize=16,color="green",shape="box"];822[label="nubNub'1 wx84 wx85 (wx86 : wx87) (foldr (||) False (((==) wx84 wx88) : map ((==) wx84) wx89))\n  Eq a",fontsize=16,color="black",shape="triangle"];822 -> 859[label="",style="solid", color="black", weight=3];
454[label="nubNub'1 wx5 wx6 [] False\n  Eq a",fontsize=16,color="black",shape="box"];454 -> 461[label="",style="solid", color="black", weight=3];
859 -> 860[label="",style="dashed", color="red", weight=0];
859[label="nubNub'1 wx84 wx85 (wx86 : wx87) ((||) (==) wx84 wx88 foldr (||) False (map ((==) wx84) wx89))\n  Eq a",fontsize=16,color="magenta"];859 -> 861[label="",style="dashed", color="magenta", weight=3];
859 -> 862[label="",style="dashed", color="magenta", weight=3];
859 -> 863[label="",style="dashed", color="magenta", weight=3];
859 -> 864[label="",style="dashed", color="magenta", weight=3];
859 -> 865[label="",style="dashed", color="magenta", weight=3];
859 -> 866[label="",style="dashed", color="magenta", weight=3];
461[label="nubNub'0 wx5 wx6 [] otherwise\n  Eq a",fontsize=16,color="black",shape="box"];461 -> 478[label="",style="solid", color="black", weight=3];
861[label="wx86\n  Eq a",fontsize=16,color="green",shape="box"];862[label="(==) wx84 wx88\n  Eq a",fontsize=16,color="blue",shape="box"];948[label="== :: ([] a) -> ([] a) -> Bool",fontsize=10,color="white",style="solid",shape="box"];862 -> 948[label="",style="solid", color="blue", weight=9];
948 -> 867[label="",style="solid", color="blue", weight=3];
949[label="== :: Double -> Double -> Bool",fontsize=10,color="white",style="solid",shape="box"];862 -> 949[label="",style="solid", color="blue", weight=9];
949 -> 868[label="",style="solid", color="blue", weight=3];
950[label="== :: () -> () -> Bool",fontsize=10,color="white",style="solid",shape="box"];862 -> 950[label="",style="solid", color="blue", weight=9];
950 -> 869[label="",style="solid", color="blue", weight=3];
951[label="== :: (Either a b) -> (Either a b) -> Bool",fontsize=10,color="white",style="solid",shape="box"];862 -> 951[label="",style="solid", color="blue", weight=9];
951 -> 870[label="",style="solid", color="blue", weight=3];
952[label="== :: (Maybe a) -> (Maybe a) -> Bool",fontsize=10,color="white",style="solid",shape="box"];862 -> 952[label="",style="solid", color="blue", weight=9];
952 -> 871[label="",style="solid", color="blue", weight=3];
953[label="== :: Integer -> Integer -> Bool",fontsize=10,color="white",style="solid",shape="box"];862 -> 953[label="",style="solid", color="blue", weight=9];
953 -> 872[label="",style="solid", color="blue", weight=3];
954[label="== :: (Ratio a) -> (Ratio a) -> Bool",fontsize=10,color="white",style="solid",shape="box"];862 -> 954[label="",style="solid", color="blue", weight=9];
954 -> 873[label="",style="solid", color="blue", weight=3];
955[label="== :: Float -> Float -> Bool",fontsize=10,color="white",style="solid",shape="box"];862 -> 955[label="",style="solid", color="blue", weight=9];
955 -> 874[label="",style="solid", color="blue", weight=3];
956[label="== :: Int -> Int -> Bool",fontsize=10,color="white",style="solid",shape="box"];862 -> 956[label="",style="solid", color="blue", weight=9];
956 -> 875[label="",style="solid", color="blue", weight=3];
957[label="== :: ((@3) a b c) -> ((@3) a b c) -> Bool",fontsize=10,color="white",style="solid",shape="box"];862 -> 957[label="",style="solid", color="blue", weight=9];
957 -> 876[label="",style="solid", color="blue", weight=3];
958[label="== :: Ordering -> Ordering -> Bool",fontsize=10,color="white",style="solid",shape="box"];862 -> 958[label="",style="solid", color="blue", weight=9];
958 -> 877[label="",style="solid", color="blue", weight=3];
959[label="== :: Char -> Char -> Bool",fontsize=10,color="white",style="solid",shape="box"];862 -> 959[label="",style="solid", color="blue", weight=9];
959 -> 878[label="",style="solid", color="blue", weight=3];
960[label="== :: Bool -> Bool -> Bool",fontsize=10,color="white",style="solid",shape="box"];862 -> 960[label="",style="solid", color="blue", weight=9];
960 -> 879[label="",style="solid", color="blue", weight=3];
961[label="== :: ((@2) a b) -> ((@2) a b) -> Bool",fontsize=10,color="white",style="solid",shape="box"];862 -> 961[label="",style="solid", color="blue", weight=9];
961 -> 880[label="",style="solid", color="blue", weight=3];
863[label="wx89\n  Eq a",fontsize=16,color="green",shape="box"];864[label="wx87\n  Eq a",fontsize=16,color="green",shape="box"];865[label="wx85\n  Eq a",fontsize=16,color="green",shape="box"];866[label="wx84\n  Eq a",fontsize=16,color="green",shape="box"];860[label="nubNub'1 wx97 wx98 (wx99 : wx100) ((||) wx101 foldr (||) False (map ((==) wx97) wx102))\n  Eq a",fontsize=16,color="burlywood",shape="triangle"];962[label="wx101/False",fontsize=10,color="white",style="solid",shape="box"];860 -> 962[label="",style="solid", color="burlywood", weight=9];
962 -> 881[label="",style="solid", color="burlywood", weight=3];
963[label="wx101/True",fontsize=10,color="white",style="solid",shape="box"];860 -> 963[label="",style="solid", color="burlywood", weight=9];
963 -> 882[label="",style="solid", color="burlywood", weight=3];
478[label="nubNub'0 wx5 wx6 [] True\n  Eq a",fontsize=16,color="black",shape="box"];478 -> 497[label="",style="solid", color="black", weight=3];
867[label="(==) wx84 wx88\n  Eq a",fontsize=16,color="black",shape="box"];867 -> 883[label="",style="solid", color="black", weight=3];
868[label="(==) wx84 wx88",fontsize=16,color="black",shape="box"];868 -> 884[label="",style="solid", color="black", weight=3];
869[label="(==) wx84 wx88",fontsize=16,color="black",shape="box"];869 -> 885[label="",style="solid", color="black", weight=3];
870[label="(==) wx84 wx88\n  Eq a  Eq b",fontsize=16,color="black",shape="box"];870 -> 886[label="",style="solid", color="black", weight=3];
871[label="(==) wx84 wx88\n  Eq a",fontsize=16,color="black",shape="box"];871 -> 887[label="",style="solid", color="black", weight=3];
872[label="(==) wx84 wx88",fontsize=16,color="black",shape="box"];872 -> 888[label="",style="solid", color="black", weight=3];
873[label="(==) wx84 wx88\n  Integral a",fontsize=16,color="black",shape="box"];873 -> 889[label="",style="solid", color="black", weight=3];
874[label="(==) wx84 wx88",fontsize=16,color="black",shape="box"];874 -> 890[label="",style="solid", color="black", weight=3];
875[label="(==) wx84 wx88",fontsize=16,color="black",shape="box"];875 -> 891[label="",style="solid", color="black", weight=3];
876[label="(==) wx84 wx88\n  Eq a  Eq b  Eq c",fontsize=16,color="black",shape="box"];876 -> 892[label="",style="solid", color="black", weight=3];
877[label="(==) wx84 wx88",fontsize=16,color="burlywood",shape="box"];964[label="wx84/LT",fontsize=10,color="white",style="solid",shape="box"];877 -> 964[label="",style="solid", color="burlywood", weight=9];
964 -> 893[label="",style="solid", color="burlywood", weight=3];
965[label="wx84/EQ",fontsize=10,color="white",style="solid",shape="box"];877 -> 965[label="",style="solid", color="burlywood", weight=9];
965 -> 894[label="",style="solid", color="burlywood", weight=3];
966[label="wx84/GT",fontsize=10,color="white",style="solid",shape="box"];877 -> 966[label="",style="solid", color="burlywood", weight=9];
966 -> 895[label="",style="solid", color="burlywood", weight=3];
878[label="(==) wx84 wx88",fontsize=16,color="black",shape="box"];878 -> 896[label="",style="solid", color="black", weight=3];
879[label="(==) wx84 wx88",fontsize=16,color="black",shape="box"];879 -> 897[label="",style="solid", color="black", weight=3];
880[label="(==) wx84 wx88\n  Eq a  Eq b",fontsize=16,color="black",shape="box"];880 -> 898[label="",style="solid", color="black", weight=3];
881[label="nubNub'1 wx97 wx98 (wx99 : wx100) ((||) False foldr (||) False (map ((==) wx97) wx102))\n  Eq a",fontsize=16,color="black",shape="box"];881 -> 899[label="",style="solid", color="black", weight=3];
882[label="nubNub'1 wx97 wx98 (wx99 : wx100) ((||) True foldr (||) False (map ((==) wx97) wx102))\n  Eq a",fontsize=16,color="black",shape="box"];882 -> 900[label="",style="solid", color="black", weight=3];
497[label="wx5 : nubNub' wx6 (wx5 : [])\n  Eq a",fontsize=16,color="green",shape="box"];497 -> 510[label="",style="dashed", color="green", weight=3];
883[label="error []",fontsize=16,color="red",shape="box"];884[label="error []",fontsize=16,color="red",shape="box"];885[label="error []",fontsize=16,color="red",shape="box"];886[label="error []",fontsize=16,color="red",shape="box"];887[label="error []",fontsize=16,color="red",shape="box"];888[label="error []",fontsize=16,color="red",shape="box"];889[label="error []",fontsize=16,color="red",shape="box"];890[label="error []",fontsize=16,color="red",shape="box"];891[label="error []",fontsize=16,color="red",shape="box"];892[label="error []",fontsize=16,color="red",shape="box"];893[label="(==) LT wx88",fontsize=16,color="burlywood",shape="box"];967[label="wx88/LT",fontsize=10,color="white",style="solid",shape="box"];893 -> 967[label="",style="solid", color="burlywood", weight=9];
967 -> 901[label="",style="solid", color="burlywood", weight=3];
968[label="wx88/EQ",fontsize=10,color="white",style="solid",shape="box"];893 -> 968[label="",style="solid", color="burlywood", weight=9];
968 -> 902[label="",style="solid", color="burlywood", weight=3];
969[label="wx88/GT",fontsize=10,color="white",style="solid",shape="box"];893 -> 969[label="",style="solid", color="burlywood", weight=9];
969 -> 903[label="",style="solid", color="burlywood", weight=3];
894[label="(==) EQ wx88",fontsize=16,color="burlywood",shape="box"];970[label="wx88/LT",fontsize=10,color="white",style="solid",shape="box"];894 -> 970[label="",style="solid", color="burlywood", weight=9];
970 -> 904[label="",style="solid", color="burlywood", weight=3];
971[label="wx88/EQ",fontsize=10,color="white",style="solid",shape="box"];894 -> 971[label="",style="solid", color="burlywood", weight=9];
971 -> 905[label="",style="solid", color="burlywood", weight=3];
972[label="wx88/GT",fontsize=10,color="white",style="solid",shape="box"];894 -> 972[label="",style="solid", color="burlywood", weight=9];
972 -> 906[label="",style="solid", color="burlywood", weight=3];
895[label="(==) GT wx88",fontsize=16,color="burlywood",shape="box"];973[label="wx88/LT",fontsize=10,color="white",style="solid",shape="box"];895 -> 973[label="",style="solid", color="burlywood", weight=9];
973 -> 907[label="",style="solid", color="burlywood", weight=3];
974[label="wx88/EQ",fontsize=10,color="white",style="solid",shape="box"];895 -> 974[label="",style="solid", color="burlywood", weight=9];
974 -> 908[label="",style="solid", color="burlywood", weight=3];
975[label="wx88/GT",fontsize=10,color="white",style="solid",shape="box"];895 -> 975[label="",style="solid", color="burlywood", weight=9];
975 -> 909[label="",style="solid", color="burlywood", weight=3];
896[label="error []",fontsize=16,color="red",shape="box"];897[label="error []",fontsize=16,color="red",shape="box"];898[label="error []",fontsize=16,color="red",shape="box"];899[label="nubNub'1 wx97 wx98 (wx99 : wx100) (foldr (||) False (map ((==) wx97) wx102))\n  Eq a",fontsize=16,color="burlywood",shape="box"];976[label="wx102/wx1020 : wx1021",fontsize=10,color="white",style="solid",shape="box"];899 -> 976[label="",style="solid", color="burlywood", weight=9];
976 -> 910[label="",style="solid", color="burlywood", weight=3];
977[label="wx102/[]",fontsize=10,color="white",style="solid",shape="box"];899 -> 977[label="",style="solid", color="burlywood", weight=9];
977 -> 911[label="",style="solid", color="burlywood", weight=3];
900[label="nubNub'1 wx97 wx98 (wx99 : wx100) True\n  Eq a",fontsize=16,color="black",shape="box"];900 -> 912[label="",style="solid", color="black", weight=3];
510 -> 509[label="",style="dashed", color="red", weight=0];
510[label="nubNub' wx6 (wx5 : [])\n  Eq a",fontsize=16,color="magenta"];510 -> 524[label="",style="dashed", color="magenta", weight=3];
510 -> 525[label="",style="dashed", color="magenta", weight=3];
510 -> 526[label="",style="dashed", color="magenta", weight=3];
901[label="(==) LT LT",fontsize=16,color="black",shape="box"];901 -> 913[label="",style="solid", color="black", weight=3];
902[label="(==) LT EQ",fontsize=16,color="black",shape="box"];902 -> 914[label="",style="solid", color="black", weight=3];
903[label="(==) LT GT",fontsize=16,color="black",shape="box"];903 -> 915[label="",style="solid", color="black", weight=3];
904[label="(==) EQ LT",fontsize=16,color="black",shape="box"];904 -> 916[label="",style="solid", color="black", weight=3];
905[label="(==) EQ EQ",fontsize=16,color="black",shape="box"];905 -> 917[label="",style="solid", color="black", weight=3];
906[label="(==) EQ GT",fontsize=16,color="black",shape="box"];906 -> 918[label="",style="solid", color="black", weight=3];
907[label="(==) GT LT",fontsize=16,color="black",shape="box"];907 -> 919[label="",style="solid", color="black", weight=3];
908[label="(==) GT EQ",fontsize=16,color="black",shape="box"];908 -> 920[label="",style="solid", color="black", weight=3];
909[label="(==) GT GT",fontsize=16,color="black",shape="box"];909 -> 921[label="",style="solid", color="black", weight=3];
910[label="nubNub'1 wx97 wx98 (wx99 : wx100) (foldr (||) False (map ((==) wx97) (wx1020 : wx1021)))\n  Eq a",fontsize=16,color="black",shape="box"];910 -> 922[label="",style="solid", color="black", weight=3];
911[label="nubNub'1 wx97 wx98 (wx99 : wx100) (foldr (||) False (map ((==) wx97) []))\n  Eq a",fontsize=16,color="black",shape="box"];911 -> 923[label="",style="solid", color="black", weight=3];
912 -> 509[label="",style="dashed", color="red", weight=0];
912[label="nubNub' wx98 (wx99 : wx100)\n  Eq a",fontsize=16,color="magenta"];912 -> 924[label="",style="dashed", color="magenta", weight=3];
912 -> 925[label="",style="dashed", color="magenta", weight=3];
912 -> 926[label="",style="dashed", color="magenta", weight=3];
524[label="wx5\n  Eq a",fontsize=16,color="green",shape="box"];525[label="wx6\n  Eq a",fontsize=16,color="green",shape="box"];526[label="[]\n  Eq a",fontsize=16,color="green",shape="box"];509[label="nubNub' wx15 (wx16 : wx17)\n  Eq a",fontsize=16,color="burlywood",shape="triangle"];980[label="wx15/wx150 : wx151",fontsize=10,color="white",style="solid",shape="box"];509 -> 980[label="",style="solid", color="burlywood", weight=9];
980 -> 522[label="",style="solid", color="burlywood", weight=3];
981[label="wx15/[]",fontsize=10,color="white",style="solid",shape="box"];509 -> 981[label="",style="solid", color="burlywood", weight=9];
981 -> 523[label="",style="solid", color="burlywood", weight=3];
913[label="True",fontsize=16,color="green",shape="box"];914[label="False",fontsize=16,color="green",shape="box"];915[label="False",fontsize=16,color="green",shape="box"];916[label="False",fontsize=16,color="green",shape="box"];917[label="True",fontsize=16,color="green",shape="box"];918[label="False",fontsize=16,color="green",shape="box"];919[label="False",fontsize=16,color="green",shape="box"];920[label="False",fontsize=16,color="green",shape="box"];921[label="True",fontsize=16,color="green",shape="box"];922 -> 822[label="",style="dashed", color="red", weight=0];
922[label="nubNub'1 wx97 wx98 (wx99 : wx100) (foldr (||) False (((==) wx97 wx1020) : map ((==) wx97) wx1021))\n  Eq a",fontsize=16,color="magenta"];922 -> 927[label="",style="dashed", color="magenta", weight=3];
922 -> 928[label="",style="dashed", color="magenta", weight=3];
922 -> 929[label="",style="dashed", color="magenta", weight=3];
922 -> 930[label="",style="dashed", color="magenta", weight=3];
922 -> 931[label="",style="dashed", color="magenta", weight=3];
922 -> 932[label="",style="dashed", color="magenta", weight=3];
923[label="nubNub'1 wx97 wx98 (wx99 : wx100) (foldr (||) False [])\n  Eq a",fontsize=16,color="black",shape="box"];923 -> 933[label="",style="solid", color="black", weight=3];
924[label="wx99\n  Eq a",fontsize=16,color="green",shape="box"];925[label="wx98\n  Eq a",fontsize=16,color="green",shape="box"];926[label="wx100\n  Eq a",fontsize=16,color="green",shape="box"];522[label="nubNub' (wx150 : wx151) (wx16 : wx17)\n  Eq a",fontsize=16,color="black",shape="box"];522 -> 529[label="",style="solid", color="black", weight=3];
523[label="nubNub' [] (wx16 : wx17)\n  Eq a",fontsize=16,color="black",shape="box"];523 -> 530[label="",style="solid", color="black", weight=3];
927[label="wx100\n  Eq a",fontsize=16,color="green",shape="box"];928[label="wx98\n  Eq a",fontsize=16,color="green",shape="box"];929[label="wx1020\n  Eq a",fontsize=16,color="green",shape="box"];930[label="wx1021\n  Eq a",fontsize=16,color="green",shape="box"];931[label="wx99\n  Eq a",fontsize=16,color="green",shape="box"];932[label="wx97\n  Eq a",fontsize=16,color="green",shape="box"];933[label="nubNub'1 wx97 wx98 (wx99 : wx100) False\n  Eq a",fontsize=16,color="black",shape="box"];933 -> 934[label="",style="solid", color="black", weight=3];
529[label="nubNub'2 (wx150 : wx151) (wx16 : wx17)\n  Eq a",fontsize=16,color="black",shape="box"];529 -> 539[label="",style="solid", color="black", weight=3];
530[label="nubNub'3 [] (wx16 : wx17)\n  Eq a",fontsize=16,color="black",shape="box"];530 -> 540[label="",style="solid", color="black", weight=3];
934[label="nubNub'0 wx97 wx98 (wx99 : wx100) otherwise\n  Eq a",fontsize=16,color="black",shape="box"];934 -> 935[label="",style="solid", color="black", weight=3];
539[label="nubNub'1 wx150 wx151 (wx16 : wx17) (wx150 `elem` wx16 : wx17)\n  Eq a",fontsize=16,color="black",shape="box"];539 -> 558[label="",style="solid", color="black", weight=3];
540[label="[]\n  Eq a",fontsize=16,color="green",shape="box"];935[label="nubNub'0 wx97 wx98 (wx99 : wx100) True\n  Eq a",fontsize=16,color="black",shape="box"];935 -> 936[label="",style="solid", color="black", weight=3];
558[label="nubNub'1 wx150 wx151 (wx16 : wx17) (any . (==))\n  Eq a",fontsize=16,color="black",shape="box"];558 -> 590[label="",style="solid", color="black", weight=3];
936[label="wx97 : nubNub' wx98 (wx97 : wx99 : wx100)\n  Eq a",fontsize=16,color="green",shape="box"];936 -> 937[label="",style="dashed", color="green", weight=3];
590[label="nubNub'1 wx150 wx151 (wx16 : wx17) (any ((==) wx150) (wx16 : wx17))\n  Eq a",fontsize=16,color="black",shape="box"];590 -> 598[label="",style="solid", color="black", weight=3];
937 -> 509[label="",style="dashed", color="red", weight=0];
937[label="nubNub' wx98 (wx97 : wx99 : wx100)\n  Eq a",fontsize=16,color="magenta"];937 -> 938[label="",style="dashed", color="magenta", weight=3];
937 -> 939[label="",style="dashed", color="magenta", weight=3];
937 -> 940[label="",style="dashed", color="magenta", weight=3];
598 -> 404[label="",style="dashed", color="red", weight=0];
598[label="nubNub'1 wx150 wx151 (wx16 : wx17) (or . map ((==) wx150))\n  Eq a",fontsize=16,color="magenta"];598 -> 603[label="",style="dashed", color="magenta", weight=3];
598 -> 604[label="",style="dashed", color="magenta", weight=3];
598 -> 605[label="",style="dashed", color="magenta", weight=3];
938[label="wx97\n  Eq a",fontsize=16,color="green",shape="box"];939[label="wx98\n  Eq a",fontsize=16,color="green",shape="box"];940[label="wx99 : wx100\n  Eq a",fontsize=16,color="green",shape="box"];603[label="wx151\n  Eq a",fontsize=16,color="green",shape="box"];604[label="wx16 : wx17\n  Eq a",fontsize=16,color="green",shape="box"];605[label="wx150\n  Eq a",fontsize=16,color="green",shape="box"];}

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ LetRed

            ↳ HASKELL

              ↳ Narrow

                ↳ QDP

                  ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

new_nubNub'10(wx97, wx98, wx99, wx100, True, wx102, bb) → new_nubNub'(wx98, wx99, wx100, bb)
new_nubNub'10(wx97, wx98, wx99, wx100, False, :(wx1020, wx1021), bb) → new_nubNub'1(wx97, wx98, wx99, wx100, wx1020, wx1021, bb)
new_nubNub'11(wx5, wx6, :(wx70, wx71), bd) → new_nubNub'1(wx5, wx6, wx70, wx71, wx70, wx71, bd)
new_nubNub'(:(wx150, wx151), wx16, wx17, bc) → new_nubNub'11(wx150, wx151, :(wx16, wx17), bc)
new_nubNub'10(wx97, wx98, wx99, wx100, False, [], bb) → new_nubNub'(wx98, wx97, :(wx99, wx100), bb)
new_nubNub'11(wx5, wx6, [], bd) → new_nubNub'(wx6, wx5, [], bd)
new_nubNub'1(wx84, wx85, wx86, wx87, wx88, wx89, ba) → new_nubNub'10(wx84, wx85, wx86, wx87, new_esEs(wx84, wx88, ba), wx89, ba)

The TRS R consists of the following rules:

new_esEs(wx84, wx88, app(app(app(ty_@3, cb), cc), cd)) → error([])
new_esEs(wx84, wx88, ty_Double) → error([])
new_esEs(wx84, wx88, ty_Integer) → error([])
new_esEs(LT, LT, ty_Ordering) → True
new_esEs(LT, GT, ty_Ordering) → False
new_esEs(GT, LT, ty_Ordering) → False
new_esEs(wx84, wx88, app(ty_[], be)) → error([])
new_esEs(wx84, wx88, app(app(ty_@2, ce), cf)) → error([])
new_esEs(wx84, wx88, app(ty_Ratio, ca)) → error([])
new_esEs(wx84, wx88, ty_@0) → error([])
new_esEs(wx84, wx88, ty_Char) → error([])
new_esEs(wx84, wx88, ty_Bool) → error([])
new_esEs(LT, EQ, ty_Ordering) → False
new_esEs(EQ, LT, ty_Ordering) → False
new_esEs(wx84, wx88, app(app(ty_Either, bf), bg)) → error([])
new_esEs(wx84, wx88, ty_Float) → error([])
new_esEs(EQ, EQ, ty_Ordering) → True
new_esEs(wx84, wx88, app(ty_Maybe, bh)) → error([])
new_esEs(GT, GT, ty_Ordering) → True
new_esEs(EQ, GT, ty_Ordering) → False
new_esEs(GT, EQ, ty_Ordering) → False
new_esEs(wx84, wx88, ty_Int) → error([])

The set Q consists of the following terms:

new_esEs(x0, x1, ty_Int)
new_esEs(x0, x1, app(app(ty_Either, x2), x3))
new_esEs(x0, x1, ty_Bool)
new_esEs(EQ, EQ, ty_Ordering)
new_esEs(x0, x1, ty_@0)
new_esEs(x0, x1, app(app(ty_@2, x2), x3))
new_esEs(x0, x1, ty_Float)
new_esEs(x0, x1, app(ty_[], x2))
new_esEs(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs(GT, LT, ty_Ordering)
new_esEs(LT, GT, ty_Ordering)
new_esEs(x0, x1, app(ty_Ratio, x2))
new_esEs(x0, x1, app(ty_Maybe, x2))
new_esEs(x0, x1, ty_Char)
new_esEs(x0, x1, ty_Double)
new_esEs(LT, LT, ty_Ordering)
new_esEs(EQ, GT, ty_Ordering)
new_esEs(GT, EQ, ty_Ordering)
new_esEs(GT, GT, ty_Ordering)
new_esEs(x0, x1, ty_Integer)
new_esEs(LT, EQ, ty_Ordering)
new_esEs(EQ, LT, ty_Ordering)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ LetRed

            ↳ HASKELL

              ↳ Narrow

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_nubNub'10(wx97, wx98, wx99, wx100, True, wx102, bb) → new_nubNub'(wx98, wx99, wx100, bb)
new_nubNub'10(wx97, wx98, wx99, wx100, False, :(wx1020, wx1021), bb) → new_nubNub'1(wx97, wx98, wx99, wx100, wx1020, wx1021, bb)
new_nubNub'11(wx5, wx6, :(wx70, wx71), bd) → new_nubNub'1(wx5, wx6, wx70, wx71, wx70, wx71, bd)
new_nubNub'(:(wx150, wx151), wx16, wx17, bc) → new_nubNub'11(wx150, wx151, :(wx16, wx17), bc)
new_nubNub'10(wx97, wx98, wx99, wx100, False, [], bb) → new_nubNub'(wx98, wx97, :(wx99, wx100), bb)
new_nubNub'1(wx84, wx85, wx86, wx87, wx88, wx89, ba) → new_nubNub'10(wx84, wx85, wx86, wx87, new_esEs(wx84, wx88, ba), wx89, ba)

The TRS R consists of the following rules:

new_esEs(wx84, wx88, app(app(app(ty_@3, cb), cc), cd)) → error([])
new_esEs(wx84, wx88, ty_Double) → error([])
new_esEs(wx84, wx88, ty_Integer) → error([])
new_esEs(LT, LT, ty_Ordering) → True
new_esEs(LT, GT, ty_Ordering) → False
new_esEs(GT, LT, ty_Ordering) → False
new_esEs(wx84, wx88, app(ty_[], be)) → error([])
new_esEs(wx84, wx88, app(app(ty_@2, ce), cf)) → error([])
new_esEs(wx84, wx88, app(ty_Ratio, ca)) → error([])
new_esEs(wx84, wx88, ty_@0) → error([])
new_esEs(wx84, wx88, ty_Char) → error([])
new_esEs(wx84, wx88, ty_Bool) → error([])
new_esEs(LT, EQ, ty_Ordering) → False
new_esEs(EQ, LT, ty_Ordering) → False
new_esEs(wx84, wx88, app(app(ty_Either, bf), bg)) → error([])
new_esEs(wx84, wx88, ty_Float) → error([])
new_esEs(EQ, EQ, ty_Ordering) → True
new_esEs(wx84, wx88, app(ty_Maybe, bh)) → error([])
new_esEs(GT, GT, ty_Ordering) → True
new_esEs(EQ, GT, ty_Ordering) → False
new_esEs(GT, EQ, ty_Ordering) → False
new_esEs(wx84, wx88, ty_Int) → error([])

The set Q consists of the following terms:

new_esEs(x0, x1, ty_Int)
new_esEs(x0, x1, app(app(ty_Either, x2), x3))
new_esEs(x0, x1, ty_Bool)
new_esEs(EQ, EQ, ty_Ordering)
new_esEs(x0, x1, ty_@0)
new_esEs(x0, x1, app(app(ty_@2, x2), x3))
new_esEs(x0, x1, ty_Float)
new_esEs(x0, x1, app(ty_[], x2))
new_esEs(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs(GT, LT, ty_Ordering)
new_esEs(LT, GT, ty_Ordering)
new_esEs(x0, x1, app(ty_Ratio, x2))
new_esEs(x0, x1, app(ty_Maybe, x2))
new_esEs(x0, x1, ty_Char)
new_esEs(x0, x1, ty_Double)
new_esEs(LT, LT, ty_Ordering)
new_esEs(EQ, GT, ty_Ordering)
new_esEs(GT, EQ, ty_Ordering)
new_esEs(GT, GT, ty_Ordering)
new_esEs(x0, x1, ty_Integer)
new_esEs(LT, EQ, ty_Ordering)
new_esEs(EQ, LT, ty_Ordering)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_nubNub'11(wx5, wx6, :(wx70, wx71), bd) → new_nubNub'1(wx5, wx6, wx70, wx71, wx70, wx71, bd)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 3 > 4, 3 > 5, 3 > 6, 4 >= 7
new_nubNub'1(wx84, wx85, wx86, wx87, wx88, wx89, ba) → new_nubNub'10(wx84, wx85, wx86, wx87, new_esEs(wx84, wx88, ba), wx89, ba)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 6 >= 6, 7 >= 7
new_nubNub'(:(wx150, wx151), wx16, wx17, bc) → new_nubNub'11(wx150, wx151, :(wx16, wx17), bc)
The graph contains the following edges 1 > 1, 1 > 2, 4 >= 4
new_nubNub'10(wx97, wx98, wx99, wx100, False, :(wx1020, wx1021), bb) → new_nubNub'1(wx97, wx98, wx99, wx100, wx1020, wx1021, bb)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 6 > 5, 6 > 6, 7 >= 7
new_nubNub'10(wx97, wx98, wx99, wx100, True, wx102, bb) → new_nubNub'(wx98, wx99, wx100, bb)
The graph contains the following edges 2 >= 1, 3 >= 2, 4 >= 3, 7 >= 4
new_nubNub'10(wx97, wx98, wx99, wx100, False, [], bb) → new_nubNub'(wx98, wx97, :(wx99, wx100), bb)
The graph contains the following edges 2 >= 1, 1 >= 2, 7 >= 4

nub'1	x xs ls True	= nub' xs ls
nub'1	x xs ls False	= nub'0 x xs ls otherwise

nubNub'	[] vw	= nubNub'3 [] vw
nubNub'	(x : xs) ls	= nubNub'2 (x : xs) ls

nubNub'1	x xs ls True	= nubNub' xs ls
nubNub'1	x xs ls False	= nubNub'0 x xs ls otherwise